|
In logic and mathematics second-order logic is an extension of first-order logic, which itself is an extension of propositional logic.〔Shapiro (1991) and Hinman (2005) give complete introductions to the subject, with full definitions.〕 Second-order logic is in turn extended by higher-order logic and type theory. First-order logic quantifies only variables that range over individuals (elements of the domain of discourse); second-order logic, in addition, also quantifies over relations. For example, the second-order sentence says that for every unary relation (or set) ''P'' of individuals, and every individual ''x'', either ''x'' is in ''P'' or it is not (this is the principle of bivalence). Second-order logic also includes quantification over functions, and other variables as explained in the section ''Syntax and fragments'' below. Both first-order and second-order logic use the idea of a domain of discourse (often called simply the "domain" or the "universe"). The domain is a set of individual elements which can be quantified over. ==Syntax and fragments== The syntax of second-order logic tells which expressions are well formed formulas. In addition to the syntax of first-order logic, second-order logic includes many new sorts (sometimes called types) of variables. These are: * A sort of variables that range over sets of individuals. If ''S'' is a variable of this sort and ''t'' is a first-order term then the expression ''t'' ∈ ''S'' (also written ''S''(''t''), or ''St'' to save parentheses) is an atomic formula. Sets of individuals can also be viewed as unary relations on the domain. * For each natural number ''k'' there is a sort of variables that ranges over all ''k''-ary relations on the individuals. If ''R'' is such a ''k''-ary relation variable and ''t''1,..., ''t''''k'' are first-order terms then the expression ''R''(''t''1,...,''t''''k'') is an atomic formula. * For each natural number ''k'' there is a sort of variables that ranges over all functions taking ''k'' elements of the domain and returning a single element of the domain. If ''f'' is such a ''k''-ary function variable and ''t''1,...,''t''''k'' are first-order terms then the expression ''f''(''t''1,...,''t''''k'') is a first-order term. Each of the variables just defined may be universally and/or existentially quantified over, to build up formulas. Thus there are many kinds of quantifiers, two for each sort of variables. A sentence in second-order logic, as in first-order logic, is a well-formed formula with no free variables (of any sort). It's possible to forgo the introduction of function variables in the definition given above (and some authors do this) because an ''n''-ary function variable can be represented by a relation variable of arity ''n''+1 and an appropriate formula for the uniqueness of the "result" in the ''n''+1 argument of the relation. (Shapiro 2000, p. 63) Monadic second-order logic (MSOL) is a restriction of second-order logic in which only quantification over unary relations (i.e.: sets) are allowed. Quantification over functions, owing to the equivalence to relations as described above, is thus also not allowed. The second-order logic without these restrictions is sometimes called full second-order logic to distinguish it from the monadic version. Monadic second-order logic is particularly used in the context of Courcelle's theorem, an algorithmic meta-theorem in graph theory. Just as in first-order logic, second-order logic may include non-logical symbols in a particular second-order language. These are restricted, however, in that all terms that they form must be either first-order terms (which can be substituted for a first-order variable) or second-order terms (which can be substituted for a second-order variable of an appropriate sort). A formula in second-order logic is said to be of first-order (and sometimes denoted or ) if its quantifiers (which may be of either type) range only over variables of first order, although it may have free variables of second order. A (existential second-order) formula is one additionally having some existential quantifiers over second order variables, i.e. , where is a first-order formula. The fragment of second order logic consisting only of existential second-order formulas is called existential second-order logic and abbreviated as ESO, as , or even as ∃SO. The fragment of formulas is defined dually, it is called universal second-order logic. More expressive fragments are defined for any ''k'' > 0 by mutual recursion: has the form , where is a formula, and similar, has the form , where is a formula. (See analytical hierarchy for the analogous construction of second-order arithmetic.) 抄文引用元・出典: フリー百科事典『 ウィキペディア(Wikipedia)』 ■ウィキペディアで「Second-order logic」の詳細全文を読む スポンサード リンク
|